/******************************************************
Compile : gcc -O3 -o pattern pattern.c io.c ksat.c enhance-sim.c sat-utils.c utils.c wrapper-minisat.c solver.c solver-utils.c -lm
******************************************************/

#include "infer.h"
#include "ksat.h"
#include "wrapper-minisat.h"
#include <stdio.h>
#include <stdlib.h>
#include <string.h>

void print_help ()
{
	printf ("Usage          : ./pattern inputfile patternfile trigger model n\n");
	printf ("                (./pattern input2 A 1 3 1)\n\n");
	printf ("trigger        : 1 first node is a trigger node\n");
	printf ("model          : 0 SIM; 1 SIM + Reliable Trans; 2 SIM + Convergence; 3 SIM + Reliable Trans + Convergence\n");
	printf ("n              : extract n nodes from patternfile\n");
	printf ("Note           : This program will extract patternfile.\n\n");
}

/* return value: 1 feasible; 0 not feasible */
int do_infer (struct infer *infer, int pathway[infer->L][infer->N])
{
	int i, j, N, L, M, flag;

	N = infer->N;
	L = infer->L;

	int R1[N + 1];
	int S[L][N]; /* state variable */
	int g[N][N], r[N][N]; /* network variable ; g[i][j]/r[i][j] edge from j to i */

	struct ksat *ksat;

	ksat = setup_ksat (N, L, pathway, S, g, r, infer);

	bool st;
	int list[ksat->num_variables + 1];

	for (i = 1; i < ksat->num_variables + 1; i++)
	{
		list[i] = 0;
	}
	for (i = 1; i < L - 2; i++)
	{
		for (j = 0; j < N; j++)
		{
			if (pathway[i][j] == -1)
				list[S[i][j]] = 1;
		}
	}
        
	st = solve_ksat2 (ksat, list);

	if (st == true)
	{
		for (i = 1; i < L - 2; i++)
		{
			for (j = 0; j < N; j++)
			{
				pathway[i][j] = list[S[i][j]];
			}
		}

		flag = 1;
	}
	else
	{
		flag = 0;
	}

	free_ksat (ksat);

	return flag;
}

int *read_inputfile2 (char *filename, struct infer *infer)
{
	FILE *fp;
	char buf[256];
	int i, j, N, L, *pattern;

	N = infer->N; 

	fp = fopen (filename, "r");
	fscanf (fp, "%*s%*s%*s%d", &L);
	infer->L = L;
	fgets (buf, 256, fp);

	pattern = calloc (N * L, sizeof (int));
	for (i = 0; i < L; i++)
	{
		fgets (buf, 256, fp);
		for (j = 0; j < N; j++)
		{
			if (buf[2 * j] == '1')
				pattern[i * N + j] = 1;
			else if (buf[2 * j] == '0')
				pattern[i * N + j] = 0;
			else
				pattern[i * N + j] = -1;
		}
	}

	fclose (fp);

	return pattern;
}

void do_enumeration (struct infer *infer, int *pattern, int pathway[infer->L][infer->N], int n, int select[n], int i, int j, int flips)
{
	int N, L;

	N = infer->N;
	L = infer->L;

	if (i == n)
	{
		int pathway2[L][N];

		memcpy (pathway2, pathway, sizeof (int) * L * N);
		if (do_infer (infer, pathway2) == 1)
			print_pathway (N, L, pathway2);
		return;
	}

	/* no more flips */
	if (flips > infer->flips[select[i]])
		return;

	/* no quickflips */
	if ((infer->model == 1 || infer->model == 3) && j >= 3 + infer->trigger)
	{
		if (pathway[j - 1][select[i]] != pathway[j - 2][select[i]] && pathway[j - 2][select[i]] != pathway[j - 3][select[i]])
			return;
	}

	if (j == L)
	{
		/* check number of flips */
		if (flips != infer->flips[select[i]])
			return;

		do_enumeration (infer, pattern, pathway, n, select, i + 1, 0, 0);
		return;
	}

	if (pattern[j * N + select[i]] == -1)
	{
		int flips2;

		pathway[j][select[i]] = 0; flips2 = flips;
		if (j > 0 && pathway[j][select[i]] != pathway[j - 1][select[i]]) flips2 ++;
		do_enumeration (infer, pattern, pathway, n, select, i, j + 1, flips2);

		pathway[j][select[i]] = 1; flips2 = flips;
		if (j > 0 && pathway[j][select[i]] != pathway[j - 1][select[i]]) flips2 ++;
		do_enumeration (infer, pattern, pathway, n, select, i, j + 1, flips2);
	}
	else
	{
		if (j > 0 && pathway[j][select[i]] != pathway[j - 1][select[i]]) flips ++;
		do_enumeration (infer, pattern, pathway, n, select, i, j + 1, flips);
	}
}

int main (int argc, char *argv[])
{
	int i, j, n;
	struct infer infer;

	if (argc == 1)
	{
		print_help ();
		exit (0);
	}

	read_inputfile (argv[1], &infer);
	infer.trigger = atoi (argv[3]);
	infer.model = atoi (argv[4]);
	infer.fixL = 1;
	infer.links = 0;

	n = atoi (argv[5]);

	int p, select[n], N, L;

	int *pattern;

	pattern = read_inputfile2(argv[2], &infer);

	N = infer.N; L = infer.L;

	int pathway[L][N], flag, flag1[N], flag2[N];

	for (i = 0; i < N; i++)
	{
		flag1[i] = 0;
		for (j = 0; j < L; j++)
		{
			pathway[j][i] = pattern[j * N + i];
			if (pathway[j][i] == -1)
				flag1[i] = 1;
		}
	}

	flag = 0;
	for (i = 0; i < N; i++)
	{
		if (flag1[i] == 1)
		{
			flag2[flag] = i;
			flag ++;
		}
	}

	//printf ("Select node:");
	for (i = 0; i < n; i++)
	{
		p = (i + 1) * flag / (n + 1);
		select[i] = flag2[p];
		//printf (" %2d", select[i]); 
	}
	//printf ("\n");

	do_enumeration (&infer, pattern, pathway, n, select, 0, 0, 0);
}
